Nuprl Definition : R-self-interface
0,22
postcript
pdf
R-self-interface(
R
)
== case
R
of
==
Rnone => True
==
Rplus(
left
,
right
)=>
rec1
,
rec2
.
rec1
&
rec2
==
Rinit(
loc
,
T
,
x
,
v
)=> True
==
Rframe(
loc
,
T
,
x
,
L
)=> True
==
Rsframe(
lnk
,
tag
,
L
)=> True
==
Reffect(
loc
,
ds
,
knd
,
T
,
x
,
f
)=> True
==
Rsends(
ds
,
knd
,
T
,
l
,
dt
,
g
)=> isrcv(
knd
)
lnk(
knd
) =
l
dt
(tag(
knd
))?Void
T
==
Rpre(
loc
,
ds
,
a
,
T
,
P
)=> True
==
Raframe(
loc
,
k
,
L
)=> True
==
Rbframe(
loc
,
k
,
L
)=> True
==
Rrframe(
loc
,
x
,
L
)=> True
latex
clarification:
R-self-interface(
R
)
== case
R
of
==
Rnone => True
==
Rplus(
left
,
right
)=>
rec1
,
rec2
.
rec1
&
rec2
==
Rinit(
loc
,
T
,
x
,
v
)=> True
==
Rframe(
loc
,
T
,
x
,
L
)=> True
==
Rsframe(
lnk
,
tag
,
L
)=> True
==
Reffect(
loc
,
ds
,
knd
,
T
,
x
,
f
)=> True
==
Rsends(
ds
,
knd
,
T
,
l
,
dt
,
g
)=> isrcv(
knd
)
== Rsends(
ds
,
knd
,
T
,
l
,
dt
,
g
)=>
lnk(
knd
) =
l
IdLnk
== Rsends(
ds
,
knd
,
T
,
l
,
dt
,
g
)=>
fpf-cap(
dt
;IdDeq;tag(
knd
);Void)
T
==
Rpre(
loc
,
ds
,
a
,
T
,
P
)=> True
==
Raframe(
loc
,
k
,
L
)=> True
==
Rbframe(
loc
,
k
,
L
)=> True
==
Rrframe(
loc
,
x
,
L
)=> True
latex
Definitions
es
realizer
ind
,
P
&
Q
,
b
,
isrcv(
k
)
,
P
Q
,
s
=
t
,
IdLnk
,
lnk(
k
)
,
f
(
x
)?
z
,
IdDeq
,
tag(
k
)
,
Void
,
True
FDL editor aliases
R-self-interface
origin